es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Try(e1)  (j  L)  ((j = loc(e1)))  (the rcv(wanted message from e1 to j)  E)) 

latex

Definitions	, IdLnk, "$x", the rcv(wanted message from e1 to j), t  T, P  Q, Id, x:A. B(x), xL. P(x), P & Q, A c B, Try(e), fischer(L)
Lemmas	event system wf, fischer wf, es-E wf, f-try wf, l member wf, es-loc wf, Id wf, not wf, es-first-from wf